<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>10. Relations &mdash; The Mechanics of Proof, by Heather Macbeth</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.js"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="Index of Lean tactics" href="Index_of_Tactics.html" />
    <link rel="prev" title="9. Sets" href="09_Sets.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
</ul>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a></li>
<li class="toctree-l1"><a class="reference internal" href="03_Parity_and_Divisibility.html">3. Parity and divisibility</a></li>
<li class="toctree-l1"><a class="reference internal" href="04_Proofs_with_Structure_II.html">4. Proofs with structure, II</a></li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a></li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="08_Functions.html">8. Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="09_Sets.html">9. Sets</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">10. Relations</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#reflexive-symmetric-antisymmetric-transitive">10.1. Reflexive, symmetric, antisymmetric, transitive</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#example">10.1.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#equals-relation">10.1.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id3">10.1.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id4">10.1.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#exercises">10.1.5. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#equivalence-relations">10.2. Equivalence relations</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id6">10.2.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id7">10.2.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id8">10.2.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id9">10.2.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id10">10.2.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id11">10.2.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id12">10.2.7. Exercises</a></li>
</ul>
</li>
</ul>
</li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="Index_of_Tactics.html">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">The Mechanics of Proof</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li><span class="section-number">10. </span>Relations</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/10_Relations.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="relations">
<span id="id1"></span><h1><span class="section-number">10. </span>Relations<a class="headerlink" href="#relations" title="Permalink to this headline">&#61633;</a></h1>
<p>Just as sets provide a convenient language for properties of the objects in a type,
<em>relations</em> provide a convenient language for the properties of the pairs of objects
in a type.  This might sound dry and abstract, but such properties turn up all over
mathematics: the property of one real
number being less than another; the property of one integer being congruent to
another modulo 5; the property of one set being a subset of another; the property
of one function being inverse to another.</p>
<p>In this chapter we introduce some of the important properties which relations
themselves can have: they can be <em>reflexive</em>, <em>symmetric</em>, <em>antisymmetric</em> or
<em>transitive</em>, or any combination of these.</p>
<section id="reflexive-symmetric-antisymmetric-transitive">
<span id="properties"></span><h2><span class="section-number">10.1. </span>Reflexive, symmetric, antisymmetric, transitive<a class="headerlink" href="#reflexive-symmetric-antisymmetric-transitive" title="Permalink to this headline">&#61633;</a></h2>
<section id="example">
<h3><span class="section-number">10.1.1. </span>Example<a class="headerlink" href="#example" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A relation <span class="math notranslate nohighlight">\(\sim\)</span> on a type <span class="math notranslate nohighlight">\(X\)</span> is <em>reflexive</em>, if for all <span class="math notranslate nohighlight">\(x\)</span> of type
<span class="math notranslate nohighlight">\(X\)</span>, it is true that <span class="math notranslate nohighlight">\(x\sim x\)</span>.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that the relation <span class="math notranslate nohighlight">\(|\)</span> on <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> is reflexive.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that for all natural numbers <span class="math notranslate nohighlight">\(x\)</span>, <span class="math notranslate nohighlight">\(x\mid x\)</span>.  Indeed, let <span class="math notranslate nohighlight">\(x\)</span> be a
natural number; then <span class="math notranslate nohighlight">\(x=x\cdot 1\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">use</span> <span class="mi">1</span>
  <span class="n">ring</span>
</pre></div>
</div>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A relation <span class="math notranslate nohighlight">\(\sim\)</span> on a type <span class="math notranslate nohighlight">\(X\)</span> is <em>symmetric</em>, if for all <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> of
type <span class="math notranslate nohighlight">\(X\)</span>, if <span class="math notranslate nohighlight">\(x\sim y\)</span>, then <span class="math notranslate nohighlight">\(y\sim x\)</span>.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that the relation <span class="math notranslate nohighlight">\(|\)</span> on <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> is not symmetric.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that there exist natural numbers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> such that, <span class="math notranslate nohighlight">\(x\mid y\)</span>
and <span class="math notranslate nohighlight">\(y\mid x\)</span>.  Indeed, we have <span class="math notranslate nohighlight">\(2=1\cdot 2\)</span>, so <span class="math notranslate nohighlight">\(1\mid 2\)</span>, and
<span class="math notranslate nohighlight">\(2\cdot 0&lt;1&lt;2\cdot 1\)</span>, so <span class="math notranslate nohighlight">\(2\not \mid 1\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="mi">1</span><span class="o">,</span> <span class="mi">2</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="mi">2</span>
    <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Nat.not_dvd_of_exists_lt_and_lt</span>
    <span class="n">use</span> <span class="mi">0</span>
    <span class="n">constructor</span>
    <span class="bp">&#183;</span> <span class="n">numbers</span>
    <span class="bp">&#183;</span> <span class="n">numbers</span>
</pre></div>
</div>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A relation <span class="math notranslate nohighlight">\(\sim\)</span> on a type <span class="math notranslate nohighlight">\(X\)</span> is <em>antisymmetric</em>, if for all <span class="math notranslate nohighlight">\(x\)</span> and
<span class="math notranslate nohighlight">\(y\)</span> of type <span class="math notranslate nohighlight">\(X\)</span>, if <span class="math notranslate nohighlight">\(x\sim y\)</span> and <span class="math notranslate nohighlight">\(y\sim x\)</span>, then <span class="math notranslate nohighlight">\(x=y\)</span>.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that the relation <span class="math notranslate nohighlight">\(|\)</span> on <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> is antisymmetric.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We first note the following fact (<span class="math notranslate nohighlight">\(\star\)</span>): if <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span> are natural numbers with <span class="math notranslate nohighlight">\(m=0\)</span>
and <span class="math notranslate nohighlight">\(m\mid n\)</span>, then <span class="math notranslate nohighlight">\(m=n\)</span>.  Indeed, since <span class="math notranslate nohighlight">\(m\mid n\)</span> there exists a natural
number <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(n=mk\)</span>, and then</p>
<div class="math notranslate nohighlight">
\[\begin{split}m&amp;=0\\
&amp;=0\cdot k\\
&amp;=mk\\
&amp;=n.\end{split}\]</div>
<p>We now return to the original problem.  We must show that for all natural numbers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span>, if <span class="math notranslate nohighlight">\(x\mid y\)</span> and <span class="math notranslate nohighlight">\(y\mid x\)</span>, then <span class="math notranslate nohighlight">\(x=y\)</span>.  Indeed, let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be natural numbers and suppose <span class="math notranslate nohighlight">\(x\mid y\)</span> and <span class="math notranslate nohighlight">\(y\mid x\)</span>. If
<span class="math notranslate nohighlight">\(x=0\)</span> then by (<span class="math notranslate nohighlight">\(\star\)</span>) we are done; likewise if <span class="math notranslate nohighlight">\(y=0\)</span>.  Otherwise, <span class="math notranslate nohighlight">\(x&gt;0\)</span>,
so since <span class="math notranslate nohighlight">\(y\mid x\)</span> we have <span class="math notranslate nohighlight">\(y\le x\)</span>, and <span class="math notranslate nohighlight">\(y&gt;0\)</span>,
so since <span class="math notranslate nohighlight">\(x\mid y\)</span> we have <span class="math notranslate nohighlight">\(x\le y\)</span>,  Putting these together, <span class="math notranslate nohighlight">\(x=y\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">have</span> <span class="n">H</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">{</span><span class="n">m</span> <span class="n">n</span><span class="o">},</span> <span class="n">m</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">&#8594;</span> <span class="n">m</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="bp">&#8594;</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">n</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">m</span> <span class="n">n</span> <span class="n">h1</span> <span class="n">h2</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h2</span>
    <span class="k">calc</span> <span class="n">m</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">*</span> <span class="n">k</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">m</span> <span class="bp">*</span> <span class="n">k</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">AntiSymmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span> <span class="n">h1</span> <span class="n">h2</span>
  <span class="n">obtain</span> <span class="n">hx</span> <span class="bp">|</span> <span class="n">hx</span> <span class="o">:=</span> <span class="n">Nat.eq_zero_or_pos</span> <span class="n">x</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">H</span> <span class="n">hx</span> <span class="n">h1</span>
  <span class="n">obtain</span> <span class="n">hy</span> <span class="bp">|</span> <span class="n">hy</span> <span class="o">:=</span> <span class="n">Nat.eq_zero_or_pos</span> <span class="n">y</span>
  <span class="bp">&#183;</span> <span class="k">have</span> <span class="o">:</span> <span class="n">y</span> <span class="bp">=</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">apply</span> <span class="n">H</span> <span class="n">hy</span> <span class="n">h2</span>
    <span class="n">rw</span> <span class="o">[</span><span class="n">this</span><span class="o">]</span>
  <span class="n">apply</span> <span class="n">le_antisymm</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Nat.le_of_dvd</span> <span class="n">hy</span> <span class="n">h1</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Nat.le_of_dvd</span> <span class="n">hx</span> <span class="n">h2</span>
</pre></div>
</div>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A relation <span class="math notranslate nohighlight">\(\sim\)</span> on a type <span class="math notranslate nohighlight">\(X\)</span> is <em>transitive</em>, if for all <span class="math notranslate nohighlight">\(x\)</span>, <span class="math notranslate nohighlight">\(y\)</span> and
<span class="math notranslate nohighlight">\(z\)</span> of type <span class="math notranslate nohighlight">\(X\)</span>, if <span class="math notranslate nohighlight">\(x\sim y\)</span> and <span class="math notranslate nohighlight">\(y\sim z\)</span>, then <span class="math notranslate nohighlight">\(x\sim z\)</span>.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that the relation <span class="math notranslate nohighlight">\(|\)</span> on <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> is transitive.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that for all natural numbers <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(c\)</span>, if <span class="math notranslate nohighlight">\(a\mid b\)</span>
and <span class="math notranslate nohighlight">\(b\mid c\)</span> then <span class="math notranslate nohighlight">\(a\mid c\)</span>.</p>
<p>Indeed, let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(c\)</span> be natural numbers with these properties.  Since
<span class="math notranslate nohighlight">\(a\mid b\)</span> there exists a natural number <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(b=ak\)</span>, and since
<span class="math notranslate nohighlight">\(b\mid c\)</span> there exists a natural number <span class="math notranslate nohighlight">\(l\)</span> such that <span class="math notranslate nohighlight">\(c=bl\)</span>.  We then have</p>
<div class="math notranslate nohighlight">
\[\begin{split}c&amp;=bl\\
&amp;=(ak)l\\
&amp;=a(kl),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(a\mid c\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="n">hab</span> <span class="n">hbc</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hab</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">l</span><span class="o">,</span> <span class="n">hl</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hbc</span>
  <span class="n">use</span> <span class="n">k</span> <span class="bp">*</span> <span class="n">l</span>
  <span class="k">calc</span> <span class="n">c</span> <span class="bp">=</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">l</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hl</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">k</span><span class="o">)</span> <span class="bp">*</span> <span class="n">l</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="o">(</span><span class="n">k</span> <span class="bp">*</span> <span class="n">l</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="equals-relation">
<span id="id2"></span><h3><span class="section-number">10.1.2. </span>Example<a class="headerlink" href="#equals-relation" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(=\)</span> on <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>:</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8477;</span><span class="o">)</span> <span class="bp">=</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">ring</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8477;</span><span class="o">)</span> <span class="bp">=</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span> <span class="n">h</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8477;</span><span class="o">)</span> <span class="bp">=</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">AntiSymmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span> <span class="n">h1</span> <span class="n">h2</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8477;</span><span class="o">)</span> <span class="bp">=</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span> <span class="n">z</span> <span class="n">h1</span> <span class="n">h2</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">,</span> <span class="n">h2</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id3">
<h3><span class="section-number">10.1.3. </span>Example<a class="headerlink" href="#id3" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>, defined by, <span class="math notranslate nohighlight">\(x\sim y\)</span> if <span class="math notranslate nohighlight">\((x-y)^2\leq 1\)</span>:</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">x</span> <span class="bp">-</span> <span class="n">y</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8804;</span> <span class="mi">1</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="k">calc</span> <span class="o">(</span><span class="n">x</span> <span class="bp">-</span> <span class="n">x</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span> <span class="n">h</span>
  <span class="k">calc</span> <span class="o">(</span><span class="n">y</span> <span class="bp">-</span> <span class="n">x</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="o">(</span><span class="n">x</span> <span class="bp">-</span> <span class="n">y</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">AntiSymmetric</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="mi">1</span><span class="o">,</span> <span class="mi">1</span><span class="bp">.</span><span class="mi">1</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="mi">1</span><span class="o">,</span> <span class="mi">1</span><span class="bp">.</span><span class="mi">9</span><span class="o">,</span> <span class="mi">2</span><span class="bp">.</span><span class="mi">5</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id4">
<h3><span class="section-number">10.1.4. </span>Example<a class="headerlink" href="#id4" title="Permalink to this headline">&#61633;</a></h3>
<p>Consider the following finite inductive type Hand.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span> <span class="n">Hand</span>
  <span class="bp">|</span> <span class="n">rock</span>
  <span class="bp">|</span> <span class="n">paper</span>
  <span class="bp">|</span> <span class="n">scissors</span>
</pre></div>
</div>
<p>Consider the following relation <span class="math notranslate nohighlight">\(\prec\)</span> on the Hand type.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[reducible]</span> <span class="kd">def</span> <span class="n">r</span> <span class="o">:</span> <span class="n">Hand</span> <span class="bp">&#8594;</span> <span class="n">Hand</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span>
  <span class="bp">|</span> <span class="n">rock</span><span class="o">,</span> <span class="n">rock</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">rock</span><span class="o">,</span> <span class="n">paper</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">rock</span><span class="o">,</span> <span class="n">scissors</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">paper</span><span class="o">,</span> <span class="n">rock</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">paper</span><span class="o">,</span> <span class="n">paper</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">paper</span><span class="o">,</span> <span class="n">scissors</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">scissors</span><span class="o">,</span> <span class="n">rock</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">scissors</span><span class="o">,</span> <span class="n">paper</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">scissors</span><span class="o">,</span> <span class="n">scissors</span> <span class="bp">=&gt;</span> <span class="n">False</span>

<span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot; &#8826; &quot;</span> <span class="bp">=&gt;</span> <span class="n">r</span>
</pre></div>
</div>
<figure class="align-default">
<img alt="_images/rock-paper-scissors.svg" src="_images/rock-paper-scissors.svg" /></figure>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\prec\)</span>:</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="n">rock</span>
  <span class="n">exhaust</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="n">rock</span><span class="o">,</span> <span class="n">paper</span>
  <span class="n">exhaust</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">AntiSymmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span>
  <span class="n">cases</span> <span class="n">x</span> <span class="bp">&lt;;&gt;</span> <span class="n">cases</span> <span class="n">y</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="n">rock</span><span class="o">,</span> <span class="n">paper</span><span class="o">,</span> <span class="n">scissors</span>
  <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="exercises">
<h3><span class="section-number">10.1.5. </span>Exercises<a class="headerlink" href="#exercises" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Show that the relation <span class="math notranslate nohighlight">\(&lt;\)</span> on <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is not symmetric.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">((</span><span class="bp">&#183;</span><span class="o">:</span><span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&lt;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>, defined by, <span class="math notranslate nohighlight">\(x\sim y\)</span> if
<span class="math notranslate nohighlight">\(x\equiv y \mod 2\)</span>, is not antisymmetric.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">&#8801;</span> <span class="n">y</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the following finite inductive type Little, and the following relation <span class="math notranslate nohighlight">\(\sim\)</span> on
the Little type. Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\sim\)</span>:</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">inductive</span> <span class="n">Little</span>
  <span class="bp">|</span> <span class="n">meg</span>
  <span class="bp">|</span> <span class="n">jo</span>
  <span class="bp">|</span> <span class="n">beth</span>
  <span class="bp">|</span> <span class="n">amy</span>
  <span class="n">deriving</span> <span class="n">DecidableEq</span>

<span class="kn">open</span> <span class="n">Little</span>

<span class="kd">@[reducible]</span> <span class="kd">def</span> <span class="n">s</span> <span class="o">:</span> <span class="n">Little</span> <span class="bp">&#8594;</span> <span class="n">Little</span> <span class="bp">&#8594;</span> <span class="kt">Prop</span>
  <span class="bp">|</span> <span class="n">meg</span><span class="o">,</span> <span class="n">meg</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">meg</span><span class="o">,</span> <span class="n">jo</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">meg</span><span class="o">,</span> <span class="n">beth</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">meg</span><span class="o">,</span> <span class="n">amy</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">jo</span><span class="o">,</span> <span class="n">meg</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">jo</span><span class="o">,</span> <span class="n">jo</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">jo</span><span class="o">,</span> <span class="n">beth</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">jo</span><span class="o">,</span> <span class="n">amy</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">beth</span><span class="o">,</span> <span class="n">meg</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">beth</span><span class="o">,</span> <span class="n">jo</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">beth</span><span class="o">,</span> <span class="n">beth</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">beth</span><span class="o">,</span> <span class="n">amy</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">amy</span><span class="o">,</span> <span class="n">meg</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">amy</span><span class="o">,</span> <span class="n">jo</span> <span class="bp">=&gt;</span> <span class="n">False</span>
  <span class="bp">|</span> <span class="n">amy</span><span class="o">,</span> <span class="n">beth</span> <span class="bp">=&gt;</span> <span class="n">True</span>
  <span class="bp">|</span> <span class="n">amy</span><span class="o">,</span> <span class="n">amy</span> <span class="bp">=&gt;</span> <span class="n">True</span>

<span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot; &#8764; &quot;</span> <span class="bp">=&gt;</span> <span class="n">s</span>
</pre></div>
</div>
<figure class="align-default">
<img alt="_images/meg-jo-beth-amy.svg" src="_images/meg-jo-beth-amy.svg" /></figure>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>,
defined by, <span class="math notranslate nohighlight">\(x\sim y\)</span> if <span class="math notranslate nohighlight">\(y\equiv x+1\mod 5\)</span>:</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
<p>Also sketch (a representative portion of) this relation as a directed graph.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">y</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>,
defined by, <span class="math notranslate nohighlight">\(x\sim y\)</span> if <span class="math notranslate nohighlight">\(x+y\equiv 0\mod 3\)</span>:</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
<p>Also sketch (a representative portion of) this relation as a directed graph.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">&#8801;</span> <span class="mi">0</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\subseteq\)</span> on
<span class="math notranslate nohighlight">\(\mathcal{P}(\mathbb{N})\)</span>, the type of sets of natural numbers.</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
<p>Also sketch (a representative portion of) this relation as a directed graph.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Reflexive</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">((</span><span class="bp">&#183;</span> <span class="o">:</span> <span class="n">Set</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8838;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\prec\)</span> on <span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span>,
defined by, <span class="math notranslate nohighlight">\((x_1, y_1) \prec (x_2,y_2)\)</span> if <span class="math notranslate nohighlight">\(x_1\le x_2\)</span> and <span class="math notranslate nohighlight">\(y_1\le y_2\)</span>:</p>
<ol class="lowerroman simple">
<li><p>reflexive;</p></li>
<li><p>symmetric;</p></li>
<li><p>antisymmetric;</p></li>
<li><p>transitive.</p></li>
</ol>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8826;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">((</span><span class="n">x1</span><span class="o">,</span> <span class="n">y1</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">(</span><span class="n">x2</span><span class="o">,</span> <span class="n">y2</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">x1</span> <span class="bp">&#8804;</span> <span class="n">x2</span> <span class="bp">&#8743;</span> <span class="n">y1</span> <span class="bp">&#8804;</span> <span class="n">y2</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8826;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="equivalence-relations">
<span id="id5"></span><h2><span class="section-number">10.2. </span>Equivalence relations<a class="headerlink" href="#equivalence-relations" title="Permalink to this headline">&#61633;</a></h2>
<section id="id6">
<h3><span class="section-number">10.2.1. </span>Example<a class="headerlink" href="#id6" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A relation is an <em>equivalence relation</em>, if it is reflexive, symmetric and transitive.</p>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.
Show that the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> defined by, <span class="math notranslate nohighlight">\(x\sim y\)</span> if
<span class="math notranslate nohighlight">\(x\equiv y\mod n\)</span> is an equivalence relation.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>By <a class="reference internal" href="03_Parity_and_Divisibility.html#modeq-refl"><span class="std std-numref">Example 3.3.10</span></a>, the relation <span class="math notranslate nohighlight">\(\sim\)</span>  is reflexive.</p>
<p>By two of the exercises to <a class="reference internal" href="03_Parity_and_Divisibility.html#theory-modular"><span class="std std-numref">Section 3.3</span></a>, the
relation <span class="math notranslate nohighlight">\(\sim\)</span>  is symmetric and transitive.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span>

<span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">&#8801;</span> <span class="n">y</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.refl</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.symm</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.trans</span>
</pre></div>
</div>
<p>Let&#8217;s sketch (a portion of) this relation as a directed graph, say for <span class="math notranslate nohighlight">\(n=3\)</span>.</p>
<figure class="align-default">
<img alt="_images/mod3alt.png" src="_images/mod3alt.png" />
</figure>
<p>It&#8217;s a mess, but it&#8217;s just possible to make out a pattern: the numbers form cliques, with, for
example, &#8230; -5, -2, 1, 4, 7, &#8230; all connected to each other and to nothing else.  We introduce
the following visual shorthand for such a directed graph: when nodes are given different colours,
this represents the directed graph in which all nodes of a given colour are connected
bi-directionally to all nodes of that colour (including themselves) and to no other nodes.</p>
<figure class="align-default">
<img alt="_images/mod3.png" src="_images/mod3.png" />
</figure>
</section>
<section id="id7">
<h3><span class="section-number">10.2.2. </span>Example<a class="headerlink" href="#id7" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> defined by <span class="math notranslate nohighlight">\(a\sim b\)</span> if
<span class="math notranslate nohighlight">\(a^2=b^2\)</span> is an equivalence relation.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>For all integers <span class="math notranslate nohighlight">\(x\)</span>, we have <span class="math notranslate nohighlight">\(x^2=x^2\)</span>, so <span class="math notranslate nohighlight">\(x\sim x\)</span>.  Therefore the relation
<span class="math notranslate nohighlight">\(\sim\)</span> is reflexive.</p>
<p>For all integers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span>, we have that if <span class="math notranslate nohighlight">\(x\sim y\)</span> then <span class="math notranslate nohighlight">\(x^2=y^2\)</span>,
so <span class="math notranslate nohighlight">\(y^2=x^2\)</span>, so <span class="math notranslate nohighlight">\(y\sim z\)</span>.
Therefore the relation <span class="math notranslate nohighlight">\(\sim\)</span> is symmetric.</p>
<p>For all integers <span class="math notranslate nohighlight">\(x\)</span>, <span class="math notranslate nohighlight">\(y\)</span> and <span class="math notranslate nohighlight">\(z\)</span>, we have that if <span class="math notranslate nohighlight">\(x\sim y\)</span> and
<span class="math notranslate nohighlight">\(y\sim z\)</span> then <span class="math notranslate nohighlight">\(x^2=y^2\)</span> and <span class="math notranslate nohighlight">\(y^2=z^2\)</span>, so</p>
<div class="math notranslate nohighlight">
\[\begin{split}x^2&amp;=y^2\\
&amp;=z^2,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(x\sim z\)</span>. Therefore the relation <span class="math notranslate nohighlight">\(\sim\)</span> is transitive.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">ring</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span> <span class="n">hxy</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">hxy</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x</span> <span class="n">y</span> <span class="n">z</span> <span class="n">hxy</span> <span class="n">hyz</span>
  <span class="k">calc</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hxy</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">z</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hyz</span><span class="o">]</span>
</pre></div>
</div>
<p>If you try to sketch the directed graph for this relation, you will see that it has the same
&#8220;clique&#8221; behaviour as the previous relation.  After sketching the directed graph, sketch the
multicoloured &#8220;clique&#8221; version.</p>
</section>
<section id="id8">
<h3><span class="section-number">10.2.3. </span>Example<a class="headerlink" href="#id8" title="Permalink to this headline">&#61633;</a></h3>
<p>You have probably guessed that the colouring can be made consistent in this way for any equivalence
relation. Let&#8217;s make this mathematically rigorous.</p>
<p>Let <span class="math notranslate nohighlight">\(r\)</span> be a relation on a type <span class="math notranslate nohighlight">\(\alpha\)</span>, denoted <span class="math notranslate nohighlight">\(\sim\)</span> in infix notation.</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>For <span class="math notranslate nohighlight">\(a\)</span> in <span class="math notranslate nohighlight">\(\alpha\)</span>, the <em>equivalence class</em> of <span class="math notranslate nohighlight">\(a\)</span> (denoted <span class="math notranslate nohighlight">\([a]\)</span>) is
<span class="math notranslate nohighlight">\(\{b:\alpha\mid a\sim b\}\)</span>.</p>
</div>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>If the relation <span class="math notranslate nohighlight">\(r\)</span> is symmetric and transitive, then for all <span class="math notranslate nohighlight">\(a_1\)</span> and <span class="math notranslate nohighlight">\(a_2\)</span>,
if <span class="math notranslate nohighlight">\(a_1\sim a_2\)</span>, then <span class="math notranslate nohighlight">\([a_1]=[a_2]\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>We must show that for all <span class="math notranslate nohighlight">\(b\)</span> in <span class="math notranslate nohighlight">\(\alpha\)</span>, <span class="math notranslate nohighlight">\(a_1\sim b\)</span> if and only if
<span class="math notranslate nohighlight">\(a_2\sim b\)</span>.</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(a_1\sim b\)</span>.  Since <span class="math notranslate nohighlight">\(a_1\sim a_2\)</span>, by symmetry
<span class="math notranslate nohighlight">\(a_2\sim a_1\)</span>, and so by transitivity <span class="math notranslate nohighlight">\(a_2\sim a_1\sim b\)</span>.</p>
<p>Conversely, suppose that <span class="math notranslate nohighlight">\(a_2\sim b\)</span>.  Then since <span class="math notranslate nohighlight">\(a_1\sim a_2\)</span>, by transitivity
<span class="math notranslate nohighlight">\(a_1\sim a_2\sim b\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">notation</span><span class="o">:</span><span class="n">arg</span> <span class="s2">&quot;&#10637;&quot;</span> <span class="n">a</span> <span class="s2">&quot;&#10640;&quot;</span> <span class="bp">=&gt;</span> <span class="o">{</span> <span class="n">b</span> <span class="bp">|</span> <span class="n">a</span> <span class="bp">&#8764;</span> <span class="n">b</span> <span class="o">}</span>

<span class="kd">theorem</span> <span class="n">EquivalenceClass.eq_of_rel</span> <span class="o">(</span><span class="n">h_symm</span> <span class="o">:</span> <span class="bp">@</span><span class="n">Symmetric</span> <span class="n">&#945;</span> <span class="n">r</span><span class="o">)</span> <span class="o">(</span><span class="n">h_trans</span> <span class="o">:</span> <span class="bp">@</span><span class="n">Transitive</span> <span class="n">&#945;</span> <span class="n">r</span><span class="o">)</span>
    <span class="o">{</span><span class="n">a1</span> <span class="n">a2</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a1</span> <span class="bp">&#8764;</span> <span class="n">a2</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#10637;</span><span class="n">a1</span><span class="bp">&#10640;</span> <span class="bp">=</span> <span class="bp">&#10637;</span><span class="n">a2</span><span class="bp">&#10640;</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">b</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">ha1b</span>
    <span class="n">apply</span> <span class="n">h_trans</span> <span class="o">(</span><span class="n">y</span> <span class="o">:=</span> <span class="n">a1</span><span class="o">)</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">h_symm</span> <span class="n">ha</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">ha1b</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">ha2b</span>
    <span class="n">apply</span> <span class="n">h_trans</span> <span class="n">ha</span> <span class="n">ha2b</span>
</pre></div>
</div>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>If the relation <span class="math notranslate nohighlight">\(r\)</span> is reflexive, then every <span class="math notranslate nohighlight">\(a\)</span> is an element of its own equivalence
class: <span class="math notranslate nohighlight">\(a\in [a]\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>We must show that for all <span class="math notranslate nohighlight">\(a\)</span>, it is true that <span class="math notranslate nohighlight">\(a\sim a\)</span>, and this is the definition
of reflexivity.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">EquivalenceClass.mem_self</span> <span class="o">(</span><span class="n">h_refl</span> <span class="o">:</span> <span class="bp">@</span><span class="n">Reflexive</span> <span class="n">&#945;</span> <span class="n">r</span><span class="o">)</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#945;</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">&#8712;</span> <span class="o">{</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">|</span> <span class="n">a</span> <span class="bp">&#8764;</span> <span class="n">b</span> <span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span>
  <span class="n">apply</span> <span class="n">h_refl</span>
</pre></div>
</div>
</section>
<section id="id9">
<h3><span class="section-number">10.2.4. </span>Example<a class="headerlink" href="#id9" title="Permalink to this headline">&#61633;</a></h3>
<p>Consider the relation <span class="math notranslate nohighlight">\(=\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>.  It is an equivalence relation, by
<a class="reference internal" href="#equals-relation"><span class="std std-numref">Example 10.1.2</span></a>.</p>
<p>Exercise: Sketch this relation, by drawing (a portion of) the underlying type
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> along a line, then colouring each equivalence class in a different colour.</p>
</section>
<section id="id10">
<h3><span class="section-number">10.2.5. </span>Example<a class="headerlink" href="#id10" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\times\mathbb{N}\)</span> defined by,
<span class="math notranslate nohighlight">\((a,b)\sim(c,d)\)</span> if <span class="math notranslate nohighlight">\(a(d+1)=c(b+1)\)</span>, is an equivalence relation.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>For all <span class="math notranslate nohighlight">\((a,b)\)</span> in <span class="math notranslate nohighlight">\(\mathbb{Z}\times\mathbb{N}\)</span>, <span class="math notranslate nohighlight">\(a(b+1)=a(b+1)\)</span>, so
<span class="math notranslate nohighlight">\((a,b)\sim (a,b)\)</span>.  Therefore <span class="math notranslate nohighlight">\(\sim\)</span> is reflexive.</p>
<p>For all <span class="math notranslate nohighlight">\((a,b)\)</span> and <span class="math notranslate nohighlight">\((c,d)\)</span> in <span class="math notranslate nohighlight">\(\mathbb{Z}\times\mathbb{N}\)</span>, if
<span class="math notranslate nohighlight">\((a,b)\sim (c,d)\)</span> then <span class="math notranslate nohighlight">\(a(d+1)=c(b+1)\)</span>, so <span class="math notranslate nohighlight">\(c(b+1)=a(d+1)\)</span>, so
<span class="math notranslate nohighlight">\((c,d)\sim (a,b)\)</span>.  Therefore <span class="math notranslate nohighlight">\(\sim\)</span> is symmetric.</p>
<p>For all <span class="math notranslate nohighlight">\((a,b)\)</span>, <span class="math notranslate nohighlight">\((c,d)\)</span> and <span class="math notranslate nohighlight">\((e,f)\)</span> in <span class="math notranslate nohighlight">\(\mathbb{Z}\times\mathbb{N}\)</span>, if
<span class="math notranslate nohighlight">\((a,b)\sim (c,d)\)</span> and <span class="math notranslate nohighlight">\((c,d)\sim (e,f)\)</span> then <span class="math notranslate nohighlight">\(a(d+1)=c(b+1)\)</span> and
<span class="math notranslate nohighlight">\(c(f+1)=e(d+1)\)</span>.  We will show that <span class="math notranslate nohighlight">\(a(f+1)=e(b+1)\)</span>, which will imply that
<span class="math notranslate nohighlight">\((a,b)\sim (e,f)\)</span>, which proves the transitivity of <span class="math notranslate nohighlight">\(\sim\)</span>.</p>
<p>Since <span class="math notranslate nohighlight">\(d+1&gt;0\)</span>, it suffices to prove that
<span class="math notranslate nohighlight">\((d+1)\left[a(f+1)\right]=(d+1)\left[e(b+1)\right]\)</span>.  Let
<span class="math notranslate nohighlight">\(B:= b+1\)</span>, <span class="math notranslate nohighlight">\(D:= d+1\)</span>, and <span class="math notranslate nohighlight">\(F:= f+1\)</span>: then we know that <span class="math notranslate nohighlight">\(aD=cB\)</span> and
<span class="math notranslate nohighlight">\(cF=eD\)</span> and need to prove that <span class="math notranslate nohighlight">\(D(aF)=D(eB)\)</span>.</p>
<p>Indeed,</p>
<div class="math notranslate nohighlight">
\[\begin{split}D  (a  F) &amp;= (a  D)  F \\
  &amp; = (c  B)  F \\
  &amp; = (c  F)  B \\
  &amp; = (e  D)  B \\
  &amp; = D  (e  B).\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">((</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">c</span><span class="o">,</span> <span class="n">d</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">a</span> <span class="bp">*</span> <span class="o">(</span><span class="n">d</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">=</span> <span class="n">c</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span>
  <span class="n">dsimp</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="o">(</span><span class="n">c</span><span class="o">,</span> <span class="n">d</span><span class="o">)</span> <span class="n">h</span>
  <span class="n">dsimp</span> <span class="n">at</span> <span class="bp">*</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="o">(</span><span class="n">c</span><span class="o">,</span> <span class="n">d</span><span class="o">)</span> <span class="o">(</span><span class="n">e</span><span class="o">,</span> <span class="n">f</span><span class="o">)</span> <span class="n">h1</span> <span class="n">h2</span>
  <span class="n">dsimp</span> <span class="n">at</span> <span class="bp">*</span>
  <span class="n">set</span> <span class="n">B</span> <span class="o">:=</span> <span class="o">(</span><span class="n">b</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span>
  <span class="n">set</span> <span class="n">D</span> <span class="o">:=</span> <span class="o">(</span><span class="n">d</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span>
  <span class="n">set</span> <span class="n">F</span> <span class="o">:=</span> <span class="o">(</span><span class="n">f</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span>
  <span class="k">have</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="n">D</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">F</span><span class="o">)</span> <span class="bp">=</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">D</span><span class="o">)</span> <span class="bp">*</span> <span class="n">F</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">c</span> <span class="bp">*</span> <span class="n">B</span><span class="o">)</span> <span class="bp">*</span> <span class="n">F</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">c</span> <span class="bp">*</span> <span class="n">F</span><span class="o">)</span> <span class="bp">*</span> <span class="n">B</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">e</span> <span class="bp">*</span> <span class="n">D</span><span class="o">)</span> <span class="bp">*</span> <span class="n">B</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h2</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">D</span> <span class="bp">*</span> <span class="o">(</span><span class="n">e</span> <span class="bp">*</span> <span class="n">B</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="n">cancel</span> <span class="n">D</span> <span class="n">at</span> <span class="n">this</span>
</pre></div>
</div>
<p>Now, sketch the relation <span class="math notranslate nohighlight">\(\sim\)</span>, by drawing (a portion of) the underlying type
<span class="math notranslate nohighlight">\(\mathbb{Z}\times\mathbb{N}\)</span> in the plane, then colouring each equivalence class in a
different colour.</p>
</section>
<section id="id11">
<h3><span class="section-number">10.2.6. </span>Example<a class="headerlink" href="#id11" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>The relation <span class="math notranslate nohighlight">\(\sim\)</span> on the type of level-0 types defined by,
<span class="math notranslate nohighlight">\(\alpha\sim\beta\)</span> if there exists a bijective function <span class="math notranslate nohighlight">\(f:\alpha\to\beta\)</span>,
is an equivalence relation.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">&#945;</span> <span class="n">&#946;</span> <span class="o">:</span> <span class="kt">Type</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="bp">&#8707;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">&#945;</span> <span class="bp">&#8594;</span> <span class="n">&#946;</span><span class="o">,</span> <span class="n">Bijective</span> <span class="n">f</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Reflexive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">&#945;</span>
  <span class="n">use</span> <span class="n">id</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">bijective_iff_exists_inverse</span><span class="o">]</span>
  <span class="n">use</span> <span class="n">id</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">rfl</span>
  <span class="bp">&#183;</span> <span class="n">rfl</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Symmetric</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">&#945;</span> <span class="n">&#946;</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">f</span><span class="o">,</span> <span class="n">hf</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">bijective_iff_exists_inverse</span><span class="o">]</span> <span class="n">at</span> <span class="n">hf</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">g</span><span class="o">,</span> <span class="n">hfg1</span><span class="o">,</span> <span class="n">hfg2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hf</span>
  <span class="n">use</span> <span class="n">g</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">bijective_iff_exists_inverse</span><span class="o">]</span>
  <span class="n">use</span> <span class="n">f</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hfg2</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hfg1</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Transitive</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">&#945;</span> <span class="n">&#946;</span> <span class="n">&#947;</span> <span class="n">h1</span> <span class="n">h2</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">f1</span><span class="o">,</span> <span class="n">hf1a</span><span class="o">,</span> <span class="n">hf1b</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h1</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">f2</span><span class="o">,</span> <span class="n">hf2a</span><span class="o">,</span> <span class="n">hf2b</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h2</span>
  <span class="n">use</span> <span class="n">f2</span> <span class="bp">&#8728;</span> <span class="n">f1</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Injective.comp</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hf2a</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hf1a</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">Surjective.comp</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hf2b</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hf1b</span>
</pre></div>
</div>
</section>
<section id="id12">
<h3><span class="section-number">10.2.7. </span>Exercises<a class="headerlink" href="#id12" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Consider the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> defined by, <span class="math notranslate nohighlight">\(a\sim b\)</span> if there
exist positive integers <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span> such that
<span class="math notranslate nohighlight">\(am=bn\)</span>.</p>
<ul class="simple">
<li><p>Show that <span class="math notranslate nohighlight">\(\sim\)</span> is an equivalence relation.</p></li>
<li><p>Sketch the relation <span class="math notranslate nohighlight">\(\sim\)</span>, by drawing (a portion of) the underlying type
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> along a line, then
colouring each equivalence class in a different colour.</p></li>
</ul>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="bp">&#8707;</span> <span class="n">m</span> <span class="n">n</span><span class="o">,</span> <span class="n">m</span> <span class="bp">&gt;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">n</span> <span class="bp">&gt;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">=</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">n</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{N}^2\)</span> defined by, <span class="math notranslate nohighlight">\((a,b)\sim(c,d)\)</span> if
<span class="math notranslate nohighlight">\(a+d=b+c\)</span>.</p>
<ul class="simple">
<li><p>Show that <span class="math notranslate nohighlight">\(\sim\)</span> is an equivalence relation.</p></li>
<li><p>Sketch the relation <span class="math notranslate nohighlight">\(\sim\)</span>, by drawing  (a portion of) the underlying type
<span class="math notranslate nohighlight">\(\mathbb{N}^2\)</span> in the plane, then
colouring each equivalence class in a different colour.</p></li>
</ul>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">((</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#215;</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">c</span><span class="o">,</span> <span class="n">d</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">d</span> <span class="bp">=</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">c</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> defined by, <span class="math notranslate nohighlight">\((a,b)\sim(c,d)\)</span> if
there exist positive integers <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span> with <span class="math notranslate nohighlight">\(mb(b^2-3a^2)=nd(d^2-3c^2)\)</span>.</p>
<ul class="simple">
<li><p>Show that <span class="math notranslate nohighlight">\(\sim\)</span> is an equivalence relation.</p></li>
<li><p>Sketch the relation <span class="math notranslate nohighlight">\(\sim\)</span>, by drawing (a portion of) the underlying type
<span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> in the plane, then
colouring each equivalence class in a different colour.</p></li>
</ul>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">((</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">(</span><span class="n">c</span><span class="o">,</span> <span class="n">d</span><span class="o">)</span> <span class="bp">&#8614;</span>
  <span class="bp">&#8707;</span> <span class="n">m</span> <span class="n">n</span><span class="o">,</span> <span class="n">m</span> <span class="bp">&gt;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">n</span> <span class="bp">&gt;</span> <span class="mi">0</span> <span class="bp">&#8743;</span> <span class="n">m</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">d</span> <span class="bp">*</span> <span class="o">(</span><span class="n">d</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="09_Sets.html" class="btn btn-neutral float-left" title="9. Sets" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="Index_of_Tactics.html" class="btn btn-neutral float-right" title="Index of Lean tactics" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2022-2024, Heather Macbeth.  All rights reserved.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>